/*
					wCal - Alloy Module
								Biagio Festa
								biagio.festa@gmail.com
*/
module wCal
open util/ordering[Day]	//order relation between days


/*				USER
		An User has one Calendar.
*/	
sig User
{
	ownCalendar: one Calendar
}
{
	//all events into ownCalendar must to be linked with this user
	all e:ownCalendar.contains | this = e.owner or this in e.shared
}


/*			EVENT
		An occurrence.
		An event keeps information about its owner,
		user joined this if any, a type of place where the event will be held,
		and an temporal instant.
*/
sig Event 
{
	owner: one User,
	shared: set User,
	where: one PlaceType,
	when: one Day
}
{
	//A User cannot be owner and shared of the same Event
	owner & shared = none	

	//This event will be into owner's calendar
	this in owner.ownCalendar.contains

	//This event will be into calendar of shared users
	all u:shared | this in u.ownCalendar.contains
}


/*			CALENDAR
		It contains a set of events
*/
sig Calendar
{
	contains: set Event
}


/*			NOTIFICATION_ON_EVENT
		A notification about an event
*/
abstract sig NotificationOnEvent
{ 
	about: one Event
}


/*			JOIN_REQUEST
		If user is owner of one event, he can send a joinRequest to other user
		to invite them.
*/
sig JoinRequest extends NotificationOnEvent
{
	sender: one User,
	receiver: some User
}
{
	//No User can send a self-request
	sender & receiver = none

	//The event of the JoinRequest is an event owner of the sender
	about.owner = sender

	//The event cannot be already into Calendars of receiver users
	receiver not in about.shared

	//The event can not be in the past
	(about.when in Today.now.nexts) or (about.when = Today.now)
}


/*			PLACE_TYPE
		The place type can be either Indoor or Outdoor
*/	
abstract sig PlaceType { }
one sig IndoorPlace extends PlaceType { }
one sig OutdoorPlace extends PlaceType { }


/*
			DAY
	NOTE: We could not know the forecast weather of a TemporalInterval
*/
sig Day
{
	weather: lone WeatherCondition	//Note 'lone'.
}



/*			WEATHER_CONDITION
		It rappresents either Good weather conditions or bad conditions
*/
abstract sig WeatherCondition { }
one sig GoodCondition extends WeatherCondition { }
one sig BadCondition extends WeatherCondition {}


/*			WeatherNotification
		If an event will occur outdoor with bad weather conditions,
		then the system will notify all the partecipants of that event.
		Moreover, The system can notify only for event that will occur
		today or tomorrow.

		Note: 	I decided to add the clause 'Notification on Today' because 
					the user could create an event for the same day.
*/
sig WeatherNotification extends NotificationOnEvent
{
	to: set User
}
{
	//Notify only events that are outdoor with bad weather condition
	about.where = OutdoorPlace and about.when.weather = BadCondition

	//Notify only owner and shared user of the event
	to = (about.owner + about.shared)

	//Notify only if the event will be hold tomorrow or today.
	 about.when = Today.now.next or Today.now = about.when
}

// 	TODAY: keeps current day.
one sig Today
{
	now: one Day
}
{
	//We always know the weather situation for today
	now.weather != none
}



/*		FACT: ACalendarCanBeManagementByOnlyOneUser

	For each Calendar 'c' exists ONLY ONE user 'u' that is owner of 
	that calendar.
*/
fact OneCalendarOneUser
{
	all c:Calendar | one u:User | u.ownCalendar = c
}

/*		FACT: NoMultipleJoinRequest
	
	An User cannot send two (or more) JoinRequest about the same Event
	to same Users.
	NOTE:  An User can send to different groups of User the same JoinRequest!
	
	TODO: @PersonalNOTE: mostra questa cosa nel progetto
*/
fact NoMultipleJoinRequest
{
	all disj req1, req2: JoinRequest | req1.about = req2.about
			implies  req1.receiver & req2.receiver = none
}

/*		FACT: NoMultipleNotificationsForSameEvent
	Don't exist 2 weather notifications for same event
*/
fact NoMultipleNotififcationsForSameEvent
{
	no disj n1,n2:WeatherNotification| n1.about = n2.about
}

/*		FACT: ThereIsAWeatherNotificationPerEachBadEvent
	Per each 'bad' event (bad weather && outdoor && will be today or tomorrow)
	thene there is a Notification about it.
*/
fact ThereIsAWeatherNotificationPerEachBadEvent
{
	all e:Event | e.where = OutdoorPlace and e.when.weather = BadCondition 
				and (e.when = Today.now.next or e.when = Today.now)
					implies
		one n:WeatherNotification | n.about = e
}

/*			FACT: WeKnowWeatherConditionForAllPastDays
		We always know the weather conditions for all past days
*/
fact WeKnowWeatherConditionForAllPastDays
{
	all d:Day | d in Today.now.prevs implies d.weather != none
}



//An Event is at least into one calendar
assert AnEventIsAlwaysIntoCalendar
{
	all e:Event | some c:Calendar | e in c.contains
}
check AnEventIsAlwaysIntoCalendar for 10

//Number of Calendars is equal to Number of Users
assert NumberCalendarEqualsNumberUsers
{
	#Calendar = #User
}
check NumberCalendarEqualsNumberUsers for 5

//An user cannot receive a join request for an event already shared with him
assert CanSendARequestForEventAlreadyShared
{
	all r:JoinRequest, e:Event | r.receiver in e.shared
				=>
						r.about not in e
}
check CanSendARequestForEventAlreadyShared for 10

//Per each JoinRequest The sender is the owner of that event
assert PerEachJoinRequestTheSenderIsOwnerOftheEvent
{
	all r:JoinRequest | one e:Event | e.owner = r.sender and e = r.about
}
check PerEachJoinRequestTheSenderIsOwnerOftheEvent for 10

//Show Static world
pred showStatic() 
{
	#User = 2
	#Event = 1
	#Day = 2
}
run showStatic for 2 but exactly 0 JoinRequest, 0 WeatherNotification

//Show Static world with one event shared between all users
pred showStaticOneEventShared()
{
	#JoinRequest = 0
	#WeatherNotification = 0
	#Event = 1
	one e:Event | e.shared + e.owner = User
}
run showStaticOneEventShared for 4

//Show when occurs a JoinRequest
pred sendJoinAccepted()
{
	#JoinRequest = 1
	#WeatherNotification = 0
	#User = 2
	#Event = 1
}
run sendJoinAccepted for 3

//Show when occurs a Notification for a event in a BadDay
pred notifyBadWeather()
{
	#JoinRequest = 0
	#User = 3
	#Event = 1
	one e:Event | e.when.weather = BadCondition
}
run notifyBadWeather for 3


